$\forall$${\it the\_es}$:event\_system\{i:l\}, $j$,$e$:es{-}E(${\it the\_es}$).
\\[0ex]($\uparrow$es{-}first(${\it the\_es}$; $j$)) $\Rightarrow$ ($\neg$es{-}locl(${\it the\_es}$; $e$; $j$))